r:Rng, u, v:|r|. Dec(u = v) 

latex

Up	rings 1
Definitions of Statement	Rng
Definitions	t  T, x:A. B(x), P & Q, , P  Q, x f y, P  Q, Rng, IsEqFun(T;eq), P  Q
Lemmas	rng wf, rng car wf, rng properties, rng eq wf, assert wf, decidable functionality, decidable assert